feat(#912): MC/DC structural coverage over synth's own decision logic (RQ-57-MCDC) - #978

RQ-57-MCDC. Closes the six-release N/A on #912 by answering the question it was
actually stuck on: which surface.

The surface, decided on evidence

#912's stated blocker was structural — witness measures MC/DC on a Wasm
artifact, synth emits ARM/RV32/A64 machine code, so "run witness on synth's
output" is a category error. That is correct about synth's output and beside
the point: the decisions that ship a miscompile are in synth's own Rust, and
those compile to Wasm fine.

REJECTED — native LLVM MC/DC via -Zcoverage-options=mcdc. Not a
preference; the capability was removed from rustc.
rust-lang/rust#144999 —
"coverage: Remove all unstable support for MC/DC instrumentation", merged
2025-08-08, Rust 1.91. Probed rather than assumed, on three nightlies
(1.93/1.95/1.97-nightly): mcdc is rejected, only block|branch|condition is
accepted. condition is the trap in that family — it builds, and yields
MC/DC Conditions 0, mcdc_records: 0, and zero llvm.instrprof.mcdc.*
intrinsics in the emitted IR. cargo-llvm-cov 0.6.21 and 0.8.7 both still
pass mcdc and both fail the build.

REJECTED — witness over the Wasm fixtures synth compiles. It measures the
fixture. The discriminating test is whose source the gap rows name; gale's run
(on #912) named core::fmt::Formatter::pad_integral,
core::str::count::do_count_chars, <u64 as Display>::fmt,
pad_integral::write_prefix, wit_bindgen::rt::cabi_realloc — five
stdlib/bindgen frames and zero synth functions. A surface whose gap rows
cannot name a synth decision cannot notice a missing condition in one.

CHOSEN — witness over a wasm32-wasip1 build of synth's OWN crates.
crates/synth-mcdc-harness is a thin row driver: it links the real crates
and calls the real pub fns with inputs arriving through Wasm parameters. It
re-implements no predicate — a mirror would be exactly the vacuous-gate class
this hub keeps finding. Gap rows name synth_core::static_data_addr::resolve_owner,
synth_backend_riscv::alloc_validator::is_ret, and so on.

Unexpected upside: witness reconstructs decisions from the lowered br_if
chains, so a Rust matches! becomes a real multi-condition decision.
is_ret's matches!(op, Jalr { rd: ZERO, rs1: RA, imm: 0 }) scores as
4 conditions — source-level MC/DC would have seen nothing there.

"The right parts"

Scored, because a missed condition here has already shipped a soundness bug in
this repo:

Excluded, named not hidden:

• synth_synthesis::instruction_selector — 225 boolean-operator lines; its own
  lane, and already gated by ~30 execution differentials.
• the aarch64 bounds_check / form_ea closures (aarch64: linear-memory load/store emit NO bounds check and --safety-bounds is a no-op (all modes byte-identical) — OOB reads/writes up to 4GiB past the guest memory instead of trapping #865) — reachable only by
  driving a whole function body through the selector. Residual: the
  guard-emission class is covered on RV32, not on aarch64.
• synth_backend::wcet* decline predicates — scan_for_decline has 1
  boolean-operator line in 1061; it is match-dispatch, so MC/DC has nothing to
  say about most of it. Branch coverage is the applicable criterion there.

Measured — and the platform turned out to be part of the measurement

witness 0.42.0, wasm32-wasip1, rustc 1.96.1, the same 56 rows, two hosts:

Same toolchain version, same witness, same rows — different host. These
count decisions reconstructed from lowered Wasm, so std inlining moves
them: validate_final_allocation_rv32 presents as 9 decisions / 44 conditions
on Linux and 4 / 43 on macOS, and ensure_supported_target disappears on Linux
entirely. Only dead is identical (50), as you'd expect of "never reached".

That was not predicted — it was measured, by the first CI run, after the
local baseline had been written down. Floors are therefore the CI numbers
(re-measured, not lowered to fit), with both baselines recorded in the script so
the macOS delta is a stated fact rather than a surprise: a developer running
this locally on macOS will not meet these floors, and that is a platform delta,
not a regression.

Witness-version invariance was checked separately (0.28.0 ≡ 0.42.0 on one host),
so the tool is not what moves these.

The gate reads gap rows, not a percentage. All 31 are printed with the
vector witness says would close them. Two residuals stated explicitly:
validate_final_allocation_rv32 carries 10- and 20-condition whole-function
chains (≥21 co-designed vectors each; not claimed), and
ensure_supported_target's ISA conjunction cannot be flipped through public
constructors (no TargetSpec has family RiscV with a non-RiscV32/64 ISA).
is_ret went 3-gap → 0-gap by adding exactly the three vectors witness
printed — the gap rows are actionable, not decorative.

Why the gate scores by FUNCTION and floors COUNTS

1. The module-wide percentage is meaningless: a wasip1 link drags in
   wasi-libc + std, so the raw figure is 3/770 with 3879 dead conditions.
2. witness's source_file/source_line cannot be used for scoping — they
   are DWARF attributions of inlined code (resolve_owner's decision reports
   as static_data_addr.rs:355; it is at :274) and only a basename, so six
   crates' backend.rs collide (upstream witness#179). The manifest's
   per-branch function_name is reliable, so the gate scopes on the
   demangled symbol.
3. A ratio cannot notice a deleted condition — removing one removes its gap
   row and the percentage improves.

Declared floors = the CI platform's measured baseline, no slack:
decisions ≥ 22, conditions ≥ 130, proved ≥ 57, fully-proved ≥ 4,
dead ≤ 50.

Dead is ceilinged, not ignored. 50 scored conditions are never
evaluated — 40 in is_straight_line, whose match arms cover RV32 opcodes the
row set does not construct. Honest residual, but an unfloored residual is how
a number rots: a change that stopped reaching the segment barriers would raise
dead, lower nothing else, and pass.

Red-first potency — and the finding that a red gate proved nothing

Locally (macOS baseline 20 / 3 / 144 / 63 / 31 / 50), both restored byte-identical

(a) Delete a condition — remove the #871 fix || rs2 == Reg::RA:

mutated   dec 19  full 2  cond 142  proved 54  dead 52
FAIL x5 (decisions, conditions, proved, fully-proved, dead ceiling)

The condition-count drop is the signal a ratio-only floor cannot produce.

(b) Weaken the vector set — drop ONE row (ra_validate:14):

mutated   dec 20  full 2  cond 144  proved 62
FAIL: proved 62 < 63 ; fully-proved 2 < 3

Then on CI, where the gate actually blocks — because the local result does not obviously transfer when the same function presents as 9 decisions instead of 4

Probe 1 (mutation a) went red at the WRONG STEP. The job's own row-driver
sanity gate asserts ra_validate(4) == 1 (#871), so deleting the condition
fails there and the MC/DC measurement never ran; VCR-RA-003 RV32 went red
independently too. Three gates catching one mutation is good engineering and
no evidence that the MC/DC floors bite. Worth recording as a general
lesson: a red gate is not evidence that the gate you were testing works — read
which step failed.

Probe 2 (mutation b) isolated them — dropping a truth-table row touches no
compiler behaviour, so the failure must come from the scoring step or not at
all. Run 31821746035:

step 7  Row-driver sanity gate (host)                     success
step 8  Run the MC/DC rows under witness                  success
step 9  Score synth's own decisions against the floors    FAILURE

baseline  22  4  130  57  23  50
probe 2   22  3  130  56  24  50
FAIL: proved conditions 56 < floor 57
FAIL: fully-proved decisions 3 < floor 4

Decisions unchanged, conditions unchanged at 130 — nothing deleted — while
proved fell and one decision dropped out of full MC/DC. Coverage lost,
structure intact, caught by the MC/DC scoring step itself, on the platform the
gate blocks on.

Both probes are reverted; git diff 712f658d -- crates/ is empty and
scripts/mcdc_run.sh is byte-identical to the pre-probe tree.

Wiring

mcdc-structural-coverage CI job, witness pinned to v0.42.0, with a
non-vacuity assert (grep -qE '^TOTAL +[0-9]+') so an empty scored table cannot
print PASS. A host-side row-driver sanity test runs under cargo test --workspace,
so a driver that returned one verdict for every row would go red rather than
quietly make the whole MC/DC run vacuous.

The toolchain is pinned to 1.96.1, deliberately unlike every other job here:
the floors are counts of decisions and conditions reconstructed from lowered
Wasm, so they are sensitive to how std inlines, and @stable is a moving
target that could red the gate with no code change. Bumping the pin is allowed
and obliges a re-measure, not a lowering. (The witness-version invariance
0.28 ≡ 0.42 is evidence about witness; it does not transfer to rustc.)

The CI runs caught three real things, recorded because they are the kind of
thing that otherwise ships: ./scripts/mcdc_run.sh exited 126 on a fresh
checkout (scripts/ is mode 644 here, cf. oracle_run.py; it only ran locally
because of a chmod); the job had been on @stable; and the floors were
host-dependent in a way no amount of local measurement would have revealed.

Gates

cargo test --workspace 0 · cargo clippy --workspace --all-targets -- -D warnings 0 ·
cargo fmt --check 0 · claim_check.py 43/43 (no new load-bearing doc claim,
so the ledger is unchanged).

Full evidence: scripts/repro/mcdc_912_gate.md.

Refs #912

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L